refactor(OracleComp): make OracleComp/OracleQuery reducible over PolyFun - #490

Examples/OneTimePad/UC.lean (1)

• abbrev otpSpec (sp : ℕ) : Interaction.Spec.{0}

VCVio/Interaction/UC/Runtime.lean (1)

• private example : Spec.Fintype

VCVio/Interaction/UC/StdDoBridge.lean (2)

• theorem sampleTranscript_done (samp : Sampler m .done) :
• theorem sampleTranscript_node {X : Type}

Examples/OneTimePad/UC.lean (1)

• abbrev otpTree (sp : ℕ) : Interaction.TypeTree.{0}

Examples/ProgramLogic/ProofMode.lean (1)

• example {m : Type → Type} [Monad m] [LawfulMonad m]

VCVio/Interaction/UC/Runtime.lean (2)

• private example : TypeTree.Fintype
• private example : TypeTree.Nonempty

VCVio/Interaction/UC/StdDoBridge.lean (2)

• theorem samplePath_done (samp : Sampler m .done) :
• theorem samplePath_node {X : Type}

VCVio/OracleComp/SimSemantics/QueryImpl/Basic.lean (1)

• theorem eq_handler : QueryImpl spec m = PFunctor.Handler m spec.toPFunctor

VCVio/OracleComp/SimSemantics/StateT/StateSeparating.lean (2)

• theorem Stateful.eq_handler
• theorem runState_eq_handler_run {α : Type v} (h : QueryImpl.Stateful I E σ)

VCVio/ProgramLogic/Tactics/Common/Core.lean (1)

• def symMatchKey (e : Expr) : MetaM Expr

• noncomputable def liftSamplerToOptionT {spec : Interaction.TypeTree.{0}} in Examples/OneTimePad/UC.lean moved from L475 to L475
• noncomputable def Sampler.uniformI (spec : TypeTree.{0}) in VCVio/Interaction/UC/Runtime.lean moved from L118 to L119
• private abbrev trivCtx : Interaction.TypeTree.Node.Context.{0, 0} in VCVio/Interaction/UC/StdDoBridge.lean moved from L173 to L174
• def ofFreeM {α : Type w} (oa : PFunctor.FreeM spec.toPFunctor α) : OracleComp spec α in VCVio/OracleComp/OracleComp.lean moved from L37 to L38
• def toFreeM {α : Type w} (oa : OracleComp spec α) : PFunctor.FreeM spec.toPFunctor α in VCVio/OracleComp/OracleComp.lean moved from L43 to L42
• theorem toFreeM_ofFreeM {α : Type w} (oa : PFunctor.FreeM spec.toPFunctor α) : in VCVio/OracleComp/OracleComp.lean moved from L50 to L47
• def toPFunctor (spec : OracleSpec ι) : PFunctor in VCVio/OracleComp/OracleSpec.lean moved from L32 to L33
• lemma toPFunctor_add {ι : Type u} {ι' : Type u'} in VCVio/OracleComp/OracleSpec.lean moved from L100 to L104
• @[reducible] def Stateful in VCVio/OracleComp/SimSemantics/StateT/StateSeparating.lean moved from L40 to L41

No new style or policy violations introduced; the diff is a systematic refactoring to rename Spec to TypeTree and adjust to upstream PolyFun changes. However, several public lemmas in VCVio/OracleComp/Traversal.lean are missing declaration docstrings, contrary to the project's documentation expectations.

• Examples/OneTimePad/UC.lean: This diff renames several core types and APIs in Examples/OneTimePad/UC.lean, replacing the old Interaction.Spec, Spec.node, Spec.done, and Spec.Sampler with Interaction.TypeTree, TypeTree.node, TypeTree.done, and TypeTree.Sampler, respectively. The corresponding otpSpec is renamed to otpTree, and PFunctor.FreeM.Displayed.Decoration is replaced by TypeTree.Decoration. The field name spec in the .step
• Examples/PRGfromPRF.lean: In Examples/PRGfromPRF.lean, a show tactic was replaced with change in the proof of the private lemma simulateQ_prfReal_oracleOutputs, at the point where the goal is prfRealQueryImpl prf k (Sum.inr s) >>= _ = _. This is a purely stylistic or tactic-level refactor; no definition, theorem statement, or proof logic was altered.
• Examples/ProgramLogic/ProofMode.lean: The import VCVio.ProgramLogic.Tactics.Relational is broadened to VCVio.ProgramLogic.Tactics, and a new HandlerNormalization section demonstrates the handler_step tactic on an equality involving PFunctor.Handler.Stateful.run and a lifted query, establishing that h.run (PFunctor.FreeM.lift query) state = (h query).run state.
• VCVio/CryptoFoundations/FiatShamir/Sigma/Stateful/Compatibility.lean: In the proof of statefulPostKeygenFreshAdvantage_eq_cmaRealRunProb_signedFreshAdv, two cases (cache_some and cache_none) were simplified by replacing simpa [monad_norm] with exact. This removes an unnecessary monad_norm rewrite, making the proof more direct.
• VCVio/CryptoFoundations/ReplayFork.lean: Removed the OracleSpec.toPFunctor entry from the attribute [local reducible] directive, keeping only PFunctor.Idx reducible locally. In contextFork_success, two simp calls that previously included mem_support_freeM_pure_iff as an argument now omit it, changing how the goal is simplified in those branches. No sorry or admit appear in the diff.
• VCVio/Interaction/UC/AsyncRuntime.lean: This diff modifies AsyncRuntime.lean to rename Spec to TypeTree throughout the file. Specifically, it updates the ProcessScheduler type abbreviation, which now uses TypeTree.Sampler m (specOf st) instead of Spec.Sampler m (specOf st), and correspondingly changes the specOf field of AsyncRuntimeState from returning a Spec.{0} to a TypeTree.{0}. The runStepsAsync function and its associated theorem runStepsAsync_empty_trivial_eq are updated to accept a TypeTree.Node.Context instead of Spec.Node.Context, and the process.step st.proc field is now accessed as .tree instead of .spec. Docstrings referencing Spec-driven sampling are also updated to say TypeTree-driven. This change is part of a larger refactoring that replaces the old Spec type with a new TypeTree type in the project's interaction layer, aligning the async runtime with the renamed API.
• VCVio/Interaction/UC/AsyncSecurity.lean: Renamed Spec.Node.Context to TypeTree.Node.Context in the AsyncRun structure and its namespace variable. Replaced the field procTranscript (of type (process.step ...).spec.Transcript) with procPath (of type (process.step ...).tree.Path), and updated all uses—including the next_state constraint, the definitions of enabledAt and firedAt, the proof of fired_implies_enabled, and the proc field in SchedulerPair—to reference tree.Path instead of spec.Transcript. Corresponding documentation strings were updated to reflect the new terminology (
• VCVio/Interaction/UC/Runtime.lean: The file refactors the Spec namespace and types to TypeTree, updating the import from SpecFintype to TypeTreeFintype. Spec.Sampler and Spec.sampleTranscript become TypeTree.Sampler and TypeTree.samplePath; Sampler.uniform now requires separate TypeTree.Fintype and TypeTree.Nonempty arguments (instead of a single Spec.Fintype), and Sampler.uniformI takes two typeclass parameters. StepOver.sample and ProcessOver.runSteps are updated to reference step.tree instead of step.spec and use the new TypeTree.Sampler/TypeTree.samplePath; the inline examples are adjusted to use TypeTree.node/TypeTree.done and demonstrate synthesis of both TypeTree.Fintype and TypeTree.Nonempty instances. This change aligns the runtime with a generalized tree representation that separates finite and nonempty constraints, improving modularity without altering the overall semantics.
• VCVio/Interaction/UC/StdDoBridge.lean: The file updates all references from the old Spec namespace to the new TypeTree namespace, renaming sampleTranscript to samplePath and Spec.Sampler to TypeTree.Sampler. The associated lemmas sampleTranscript_done/node become samplePath_done/node; the spec field in the ProcessOver step example is renamed to tree. The theorems StepOver.sample_eq, ProcessOver.runSteps_zero, runSteps_succ, and runSteps_triple_preserves_invariant have their type signatures updated to use TypeTree.samplePath and TypeTree.Sampler accordingly. No new sorry or admit are introduced.
• VCVio/OracleComp/OracleComp.lean: The diff makes OracleComp itself @[reducible] (it was previously not marked reducible, while ofFreeM and toFreeM already were). It also removes three instance declarations: the Monad, LawfulMonad, and MonadLift instances for OracleComp spec that were previously defined by casting to the underlying PFunctor.FreeM instances. Finally, several theorem and definition signatures are reformatted for brevity (line breaks removed), but their statements are unchanged.
• VCVio/OracleComp/OracleQuery.lean: The OracleQuery definition is now marked @[reducible] to improve definitional unfolding and type inference. The explicit Functor and LawfulFunctor instances for OracleQuery spec have been removed, since their definitions are no longer needed given the @[reducible] attribute and the fact that OracleQuery is defined as PFunctor.Obj spec.toPFunctor, which already provides those instances via the inherited structure from PFunctor.Obj. No sorry or admit are present.
• VCVio/OracleComp/OracleSpec.lean: The diff makes two changes to VCVio/OracleComp/OracleSpec.lean. First, toPFunctor is marked @[reducible] and defined via PFunctor.mk (rather than a structure literal), increasing the API's transparency for typeclass resolution. Second, the @[simp] attribute is removed from toPFunctor_add with a comment explaining that rewriting toPFunctor inside the instance-carrying type of OracleComp under simulateQ/liftM blocks the simulateQ_query family from matching, so the lemma is deliberately not a simp lemma to avoid breaking those tactics.
• VCVio/OracleComp/QueryTracking/HandlerSimp.lean: The diff modifies HandlerSimp.lean to align the handler_simp simp set with PolyFun's generic handler_nf normal form. It adds an import of PolyFun.PFunctor.Handler.Normalization, updates the module docstring to describe handler_simp as extending handler_nf with VCVio-specific equations, and removes several StateT and WriterT simplification lemmas (StateT.run_bind, StateT.run_get, StateT.run_set, StateT.run_modifyGet, StateT.run_pure, StateT.run_monadLift, WriterT.run_bind, WriterT.run_pure, WriterT.run_tell) from the handler_simp attribute set, retaining only WriterT.run_bind', WriterT.run_monadLift, WriterT.run_monadLift', and WriterT.run_pure'. No new sorry or admit are added.
• VCVio/OracleComp/SimSemantics/QueryImpl/Basic.lean: The diff modifies VCVio/OracleComp/SimSemantics/QueryImpl/Basic.lean to connect the QueryImpl type to the PolyFun library's polynomial functor framework. It adds an import of PolyFun.PFunctor.Handler and a new theorem eq_handler, which states that QueryImpl spec m is definitionally equal to PFunctor.Handler m spec.toPFunctor. The docstring comment on QueryImpl itself is updated to describe it as a 'monadic handler for the polynomial interface induced by spec' instead of its prior wording.
• VCVio/OracleComp/SimSemantics/StateT/PreservesInv.lean: In the proof of simulateQ_run_preservesInv, the simpa tactic was updated to use the lemma simulateQ_spec_query instead of the combination OracleSpec.query_def, simulateQ_query. This change simplifies the proof by consolidating the previously used lemmas into a single lemma.
• VCVio/OracleComp/SimSemantics/StateT/StateSeparating.lean: This commit makes two main changes to StateSeparating.lean. First, the Stateful definition is marked @[reducible] to make it definitionally transparent, and a new theorem Stateful.eq_handler is added to establish that QueryImpl.Stateful I E σ is definitionally equal to PFunctor.Handler.Stateful (OracleComp I) σ E.toPFunctor. Second, a new theorem runState_eq_handler_run is added to the Stateful namespace to prove that h.runState s₀ A is definitionally equal to PFunctor.Handler.Stateful.run h A s₀; this is accompanied by a new import of PolyFun.PFunctor.Handler.Stateful.
• VCVio/OracleComp/SimSemantics/WriterT/PreservesInv.lean: The proof of simulateQ_run_writerPreservesInv was updated to replace a group of simplification lemmas (OracleSpec.query_def, ofPFunctor_toPFunctor, simulateQ_query, OracleQuery.input_apply, OracleQuery.cont_apply, id_map) with the single lemma simulateQ_spec_query. This refactors the simp call in the query_bind case, likely to align with a consolidation of query-related reasoning in the project.
• VCVio/OracleComp/Traversal.lean: This PR refactors VCVio/OracleComp/Traversal.lean to redefine allPathsSatisfy and somePathSatisfies using PFunctor.FreeM.Cursor from the PolyFun library, replacing prior inductive definitions. It adds the import PolyFun.PFunctor.Free.Cursor and updates the file’s module docstring to explain the new cursor-based phrasing: a cursor represents a typed path prefix into the free-monad tree, so quantifying over cursors whose recorded directions stay within possibleOutputs captures every demanded query node (via non-terminal cursors) and every reachable final output (via terminal cursors). The lemmas allPathsSatisfy_pure, somePathSatisfies_pure, allPathsSatisfy_query_bind, and somePathSatisfies_query_bind are rewritten to use a propext-based proof pattern involving cursor operations (PFunctor.FreeM.Cursor.root, .down, .trace_down) and TraceList.directionsWithin_cons. The auxiliary definitions allOutputsSatisfyWhen and someOutputSatisfiesWhen are changed from method invocations (oa.allPathsSatisfy) to function applications (allPathsSatisfy ... oa). The lemma allOutputsSatisfyWhen_iff_supportWhen and someOutputSatisfiesWhen_iff_supportWhen are updated accordingly, and both allPathsSatisfy_bind_iff and somePathSatisfies_bind_iff are refactored from a single-line induction with simp to an explicit pattern match using pure x and query_bind q oa ih cases, calling pure_bind and monad_norm directly.
• VCVio/Prelude.lean: Added a new declare_aesop_rule_sets [UnfoldEvalDist] invocation and changed the docstring comment for the handler_simp simp attribute from a generic description (
• VCVio/ProgramLogic/Tactics/Common/Core.lean: This diff adds a new symMatchKey function to Core.lean that normalizes reducible oracle wrappers (OracleComp, OracleQuery, OracleSpec.toPFunctor) in goal-side computations. It also adds the import import Lean.Meta.Sym.Pattern. The purpose is to ensure that goal expressions have keys matching those produced by Sym.mkPatternFromDeclWithKey, which is needed for proper Sym.DiscrTree.getMatch lookup. A comment explains that Sym.preprocessType must not be used here because it could cause panics with matchers and loose de Bruijn variables.
• VCVio/ProgramLogic/Tactics/Common/Registry.lean: In Registry.lean, three lookup functions for VC spec entries were modified to apply symMatchKey to the key expression before querying the discrimination tree: getRegisteredUnaryVCSpecEntries now calls symMatchKey after whnfReducible, getRegisteredUnaryVCSpecEntriesNoWhnf replaced its instantiateMVars call with symMatchKey, and getRegisteredRelationalVCSpecEntries now wraps symMatchKey around the reduction of oa. This ensures that the key used for tree lookup is normalized by symMatchKey, which likely expands or canonicalizes symbolic names (e.g., unfold sym projections) so that the discrimination tree matches entries registered under the underlying constant rather than the symbolic wrapper. No sorry or admit were introduced.
• VCVio/ProgramLogic/Tactics/Common/WpStepRegistry.lean: In getRegisteredWpStepEntries, a call to symMatchKey was added after whnf; in getRegisteredWpStepEntriesNoWhnf, the existing instantiateMVars call was replaced with symMatchKey. Both functions now canonicalize the expression via symMatchKey before registry lookup, ensuring consistent normalization for symbolic matching and likely fixing cases where instantiateMVars alone was insufficient.
• VCVio/ProgramLogic/Tactics/Handler.lean: The handler_step tactic's implementation was updated to apply PolyFun's generic handler_nf simplification set before VCVio's handler_simp set, replacing the previous use of only handler_simp. The documentation comment was revised to reflect this two-pass normalization strategy, which aims to expose handler bodies or run-shapes for subsequent tactics like mvcgen, vcstep, or rvcstep.
• VCVio/StateSeparating/CellRef.lean: In theorem simulateQ_run_cellPreserved, the simpa call was simplified by removing the reference to OracleSpec.query_def, leaving only simulateQ_spec_query. This eliminates an unnecessary lemma dependency, streamlining the proof.
• docs/agents/gotchas.md: Extended the existing gotcha about @[reducib le] thin wrappers by listing OracleQuery and OracleSpec.toPFunctor as newly included types, and by stating that the Monad/Functor instances come directly from PFunctor.FreeM/PFunctor.Obj. Added two detailed failure modes: (1) dot notation on monadic results fails because the inferred type is PFunctor.FreeM, not OracleComp — the workaround is to use prefix form; (2) attribute [local reducible] on a definition that instance keys mention silently breaks instance resolution (e.g. MonadLiftT (OracleComp spec) SetM vanishes). Finally, documented that OracleSpec.toPFunctor_add is deliberately not @[simp], explaining that rewriting (spec + spec').toPFunctor under simulateQ/liftM prevents the simulateQ_query family from matching.
• docs/agents/oracle-comp.md: Added a paragraph explaining that QueryImpl is definitionally equal to PFunctor.Handler m spec.toPFunctor, as recorded by QueryImpl.eq_handler, and that the source definition retains the dependent function form for better type inference in polymorphic query code. Also notes the PolyFun theorem that allows this object to interpret any free program over the interface.
• docs/agents/program-logic.md: The diff updates the documentation for the handler_step tactic: its goal shape now includes FreeM and general transformer goals (previously just QueryImpl/simulateQ/StateT), and its normalization pass uses both handler_nf and handler_simp. A new paragraph explains the ownership split between PolyFun (generic handler_nf rules) and VCVio (specific handler_simp rules) and that handler_step applies them in generic-to-specific order. Additionally, a new section titled "Key alignment invariant" documents the requirement for registry query functions to use symMatchKey (from Tactics/Common/Core.lean) to recursively unfold only OracleComp, OracleQuery, and OracleSpec.toPFunctor, because OracleComp is a reducible alias of PFunctor.FreeM and using Sym.preprocessType may cause failures; this explains why silent lookup failures can occur without the targeted normalization.
• lakefile.lean: Updated the pinned commit hash for the PolyFun dependency from 97a262ce2ba7513448b76635e1f6a07f61f40de5 to 29644990ebc2828ca09170bc9d398649cd9f5950, pulling in upstream changes.
• 1 file(s) filtered as noise (lockfiles, generated, or trivial): lake-manifest.json

Cross-file analysis failed: 400 INVALID_ARGUMENT. {'error': {'code': 400, 'message': 'API key not valid. Please pass a valid API key.', 'status': 'INVALID_ARGUMENT', 'details': [{'@type': 'type.googleapis.com/google.rpc.ErrorInfo', 'reason': 'API_KEY_INVALID', 'domain': 'googleapis.com', 'metadata': {'service': 'generativelanguage.googleapis.com'}}, {'@type': 'type.googleapis.com/google.rpc.LocalizedMessage', 'locale': 'en-US', 'message': 'API key not valid. Please pass a valid API key.'}]}}

An error occurred while analyzing Examples/PRGfromPRF.lean: 400 INVALID_ARGUMENT. {'error': {'code': 400, 'message': 'API key not valid. Please pass a valid API key.', 'status': 'INVALID_ARGUMENT', 'details': [{'@type': 'type.googleapis.com/google.rpc.ErrorInfo', 'reason': 'API_KEY_INVALID', 'domain': 'googleapis.com', 'metadata': {'service': 'generativelanguage.googleapis.com'}}, {'@type': 'type.googleapis.com/google.rpc.LocalizedMessage', 'locale': 'en-US', 'message': 'API key not valid. Please pass a valid API key.'}]}}

An error occurred while analyzing VCVio/CryptoFoundations/FiatShamir/Sigma/Stateful/Compatibility.lean: 400 INVALID_ARGUMENT. {'error': {'code': 400, 'message': 'API key not valid. Please pass a valid API key.', 'status': 'INVALID_ARGUMENT', 'details': [{'@type': 'type.googleapis.com/google.rpc.ErrorInfo', 'reason': 'API_KEY_INVALID', 'domain': 'googleapis.com', 'metadata': {'service': 'generativelanguage.googleapis.com'}}, {'@type': 'type.googleapis.com/google.rpc.LocalizedMessage', 'locale': 'en-US', 'message': 'API key not valid. Please pass a valid API key.'}]}}

An error occurred while analyzing VCVio/CryptoFoundations/ReplayFork.lean: 400 INVALID_ARGUMENT. {'error': {'code': 400, 'message': 'API key not valid. Please pass a valid API key.', 'status': 'INVALID_ARGUMENT', 'details': [{'@type': 'type.googleapis.com/google.rpc.ErrorInfo', 'reason': 'API_KEY_INVALID', 'domain': 'googleapis.com', 'metadata': {'service': 'generativelanguage.googleapis.com'}}, {'@type': 'type.googleapis.com/google.rpc.LocalizedMessage', 'locale': 'en-US', 'message': 'API key not valid. Please pass a valid API key.'}]}}

An error occurred while analyzing VCVio/OracleComp/OracleComp.lean: 400 INVALID_ARGUMENT. {'error': {'code': 400, 'message': 'API key not valid. Please pass a valid API key.', 'status': 'INVALID_ARGUMENT', 'details': [{'@type': 'type.googleapis.com/google.rpc.ErrorInfo', 'reason': 'API_KEY_INVALID', 'domain': 'googleapis.com', 'metadata': {'service': 'generativelanguage.googleapis.com'}}, {'@type': 'type.googleapis.com/google.rpc.LocalizedMessage', 'locale': 'en-US', 'message': 'API key not valid. Please pass a valid API key.'}]}}

An error occurred while analyzing VCVio/OracleComp/OracleQuery.lean: 400 INVALID_ARGUMENT. {'error': {'code': 400, 'message': 'API key not valid. Please pass a valid API key.', 'status': 'INVALID_ARGUMENT', 'details': [{'@type': 'type.googleapis.com/google.rpc.ErrorInfo', 'reason': 'API_KEY_INVALID', 'domain': 'googleapis.com', 'metadata': {'service': 'generativelanguage.googleapis.com'}}, {'@type': 'type.googleapis.com/google.rpc.LocalizedMessage', 'locale': 'en-US', 'message': 'API key not valid. Please pass a valid API key.'}]}}

An error occurred while analyzing VCVio/OracleComp/OracleSpec.lean: 400 INVALID_ARGUMENT. {'error': {'code': 400, 'message': 'API key not valid. Please pass a valid API key.', 'status': 'INVALID_ARGUMENT', 'details': [{'@type': 'type.googleapis.com/google.rpc.ErrorInfo', 'reason': 'API_KEY_INVALID', 'domain': 'googleapis.com', 'metadata': {'service': 'generativelanguage.googleapis.com'}}, {'@type': 'type.googleapis.com/google.rpc.LocalizedMessage', 'locale': 'en-US', 'message': 'API key not valid. Please pass a valid API key.'}]}}

An error occurred while analyzing VCVio/OracleComp/SimSemantics/StateT/PreservesInv.lean: 400 INVALID_ARGUMENT. {'error': {'code': 400, 'message': 'API key not valid. Please pass a valid API key.', 'status': 'INVALID_ARGUMENT', 'details': [{'@type': 'type.googleapis.com/google.rpc.ErrorInfo', 'reason': 'API_KEY_INVALID', 'domain': 'googleapis.com', 'metadata': {'service': 'generativelanguage.googleapis.com'}}, {'@type': 'type.googleapis.com/google.rpc.LocalizedMessage', 'locale': 'en-US', 'message': 'API key not valid. Please pass a valid API key.'}]}}

An error occurred while analyzing VCVio/OracleComp/SimSemantics/WriterT/PreservesInv.lean: 400 INVALID_ARGUMENT. {'error': {'code': 400, 'message': 'API key not valid. Please pass a valid API key.', 'status': 'INVALID_ARGUMENT', 'details': [{'@type': 'type.googleapis.com/google.rpc.ErrorInfo', 'reason': 'API_KEY_INVALID', 'domain': 'googleapis.com', 'metadata': {'service': 'generativelanguage.googleapis.com'}}, {'@type': 'type.googleapis.com/google.rpc.LocalizedMessage', 'locale': 'en-US', 'message': 'API key not valid. Please pass a valid API key.'}]}}

An error occurred while analyzing VCVio/OracleComp/Traversal.lean: 400 INVALID_ARGUMENT. {'error': {'code': 400, 'message': 'API key not valid. Please pass a valid API key.', 'status': 'INVALID_ARGUMENT', 'details': [{'@type': 'type.googleapis.com/google.rpc.ErrorInfo', 'reason': 'API_KEY_INVALID', 'domain': 'googleapis.com', 'metadata': {'service': 'generativelanguage.googleapis.com'}}, {'@type': 'type.googleapis.com/google.rpc.LocalizedMessage', 'locale': 'en-US', 'message': 'API key not valid. Please pass a valid API key.'}]}}

An error occurred while analyzing VCVio/ProgramLogic/Tactics/Common/Core.lean: 400 INVALID_ARGUMENT. {'error': {'code': 400, 'message': 'API key not valid. Please pass a valid API key.', 'status': 'INVALID_ARGUMENT', 'details': [{'@type': 'type.googleapis.com/google.rpc.ErrorInfo', 'reason': 'API_KEY_INVALID', 'domain': 'googleapis.com', 'metadata': {'service': 'generativelanguage.googleapis.com'}}, {'@type': 'type.googleapis.com/google.rpc.LocalizedMessage', 'locale': 'en-US', 'message': 'API key not valid. Please pass a valid API key.'}]}}

An error occurred while analyzing VCVio/ProgramLogic/Tactics/Common/Registry.lean: 400 INVALID_ARGUMENT. {'error': {'code': 400, 'message': 'API key not valid. Please pass a valid API key.', 'status': 'INVALID_ARGUMENT', 'details': [{'@type': 'type.googleapis.com/google.rpc.ErrorInfo', 'reason': 'API_KEY_INVALID', 'domain': 'googleapis.com', 'metadata': {'service': 'generativelanguage.googleapis.com'}}, {'@type': 'type.googleapis.com/google.rpc.LocalizedMessage', 'locale': 'en-US', 'message': 'API key not valid. Please pass a valid API key.'}]}}

An error occurred while analyzing VCVio/ProgramLogic/Tactics/Common/WpStepRegistry.lean: 400 INVALID_ARGUMENT. {'error': {'code': 400, 'message': 'API key not valid. Please pass a valid API key.', 'status': 'INVALID_ARGUMENT', 'details': [{'@type': 'type.googleapis.com/google.rpc.ErrorInfo', 'reason': 'API_KEY_INVALID', 'domain': 'googleapis.com', 'metadata': {'service': 'generativelanguage.googleapis.com'}}, {'@type': 'type.googleapis.com/google.rpc.LocalizedMessage', 'locale': 'en-US', 'message': 'API key not valid. Please pass a valid API key.'}]}}

An error occurred while analyzing VCVio/StateSeparating/CellRef.lean: 400 INVALID_ARGUMENT. {'error': {'code': 400, 'message': 'API key not valid. Please pass a valid API key.', 'status': 'INVALID_ARGUMENT', 'details': [{'@type': 'type.googleapis.com/google.rpc.ErrorInfo', 'reason': 'API_KEY_INVALID', 'domain': 'googleapis.com', 'metadata': {'service': 'generativelanguage.googleapis.com'}}, {'@type': 'type.googleapis.com/google.rpc.LocalizedMessage', 'locale': 'en-US', 'message': 'API key not valid. Please pass a valid API key.'}]}}

Examples/OneTimePad/UC.lean (1)

• abbrev otpSpec (sp : ℕ) : Interaction.Spec.{0}

VCVio/Interaction/UC/Runtime.lean (1)

• private example : Spec.Fintype

VCVio/Interaction/UC/StdDoBridge.lean (2)

• theorem sampleTranscript_done (samp : Sampler m .done) :
• theorem sampleTranscript_node {X : Type}

Examples/OneTimePad/UC.lean (1)

• abbrev otpTree (sp : ℕ) : Interaction.TypeTree.{0}

Examples/ProgramLogic/ProofMode.lean (1)

• example {m : Type → Type} [Monad m] [LawfulMonad m]

VCVio/Interaction/UC/Runtime.lean (2)

• private example : TypeTree.Fintype
• private example : TypeTree.Nonempty

VCVio/Interaction/UC/StdDoBridge.lean (2)

• theorem samplePath_done (samp : Sampler m .done) :
• theorem samplePath_node {X : Type}

VCVio/OracleComp/SimSemantics/QueryImpl/Basic.lean (1)

• theorem eq_handler : QueryImpl spec m = PFunctor.Handler m spec.toPFunctor

VCVio/OracleComp/SimSemantics/StateT/StateSeparating.lean (2)

• theorem Stateful.eq_handler
• theorem runState_eq_handler_run {α : Type v} (h : QueryImpl.Stateful I E σ)

VCVio/ProgramLogic/Tactics/Common/Core.lean (1)

• def symMatchKey (e : Expr) : MetaM Expr

• noncomputable def liftSamplerToOptionT {spec : Interaction.TypeTree.{0}} in Examples/OneTimePad/UC.lean moved from L475 to L475
• noncomputable def Sampler.uniformI (spec : TypeTree.{0}) in VCVio/Interaction/UC/Runtime.lean moved from L118 to L119
• private abbrev trivCtx : Interaction.TypeTree.Node.Context.{0, 0} in VCVio/Interaction/UC/StdDoBridge.lean moved from L173 to L174
• def ofFreeM {α : Type w} (oa : PFunctor.FreeM spec.toPFunctor α) : OracleComp spec α in VCVio/OracleComp/OracleComp.lean moved from L37 to L38
• def toFreeM {α : Type w} (oa : OracleComp spec α) : PFunctor.FreeM spec.toPFunctor α in VCVio/OracleComp/OracleComp.lean moved from L43 to L42
• theorem toFreeM_ofFreeM {α : Type w} (oa : PFunctor.FreeM spec.toPFunctor α) : in VCVio/OracleComp/OracleComp.lean moved from L50 to L47
• def toPFunctor (spec : OracleSpec ι) : PFunctor in VCVio/OracleComp/OracleSpec.lean moved from L32 to L33
• lemma toPFunctor_add {ι : Type u} {ι' : Type u'} in VCVio/OracleComp/OracleSpec.lean moved from L100 to L104
• @[reducible] def Stateful in VCVio/OracleComp/SimSemantics/StateT/StateSeparating.lean moved from L40 to L41

The diff is a large refactor/rename Spec → TypeTree across the VCVio project, plus attendant changes in OracleComp, ProgramLogic, and non-Spec/TypeTree files. The diff touches documentation, test files, and the lake-manifest/lakefile for the PolyFun dependency. Although the diff is extensive, I was asked to review against a specific set of deployment-supplied instructions (the

• Examples/OneTimePad/UC.lean: Renamed Interaction.Spec to Interaction.TypeTree throughout the file, including the abbreviation otpSpec to otpTree. Updated field names from spec to tree in the step records of msgClosed, realOtp, and idealOtp. Changed the type of otpDecoration from PFunctor.FreeM.Displayed.Decoration to TypeTree.Decoration. Updated docstrings to reflect the new terminology. In realOtp_boundaryTrace and idealOtp_boundaryTrace, changed the path type from Spec.Transcript to TypeTree.Path. In realOtp_ne_idealOtp, updated the equality comparison to use step.tree instead of step.spec. The liftSamplerToOptionT function now operates on TypeTree.Sampler instead of Spec.Sampler and uses TypeTree.Decoration.map instead of PFunctor.FreeM.Displayed.Decoration.map. No sorry or admit were introduced.
• Examples/PRGfromPRF.lean: In Examples/PRGfromPRF.lean, the proof of simulateQ_prfReal_oracleOutputs was refactored: show was replaced with change to assert the same equality about prfRealQueryImpl. This is a purely syntactic adjustment to the proof script; no theorems, definitions, signatures, or sorry/admitted declarations were added or removed.
• Examples/ProgramLogic/ProofMode.lean: The file Examples/ProgramLogic/ProofMode.lean is updated in two ways. First, the import VCVio.ProgramLogic.Tactics.Relational is replaced with the broader VCVio.ProgramLogic.Tactics. Second, a new section HandlerNormalization is added containing a single example theorem that uses handler_step to demonstrate that h.run (PFunctor.FreeM.lift query) state = (h query).run state for a PFunctor.Handler.Stateful handler, thereby exercising the new handler normalization tactic imported via the changed import.
• VCVio/CryptoFoundations/FiatShamir/Sigma/Stateful/Compatibility.lean: In statefulPostKeygenFreshAdvantage_eq_cmaRealRunProb_signedFreshAdv, the proof body was simplified: the two simpa [monad_norm] applications were replaced with direct exact calls to the auxiliary lemmas fiatShamirVerify_run_eq_cmaRealSourceFullSum_run_signedFresh_cache_some and fiatShamirVerify_run_eq_cmaRealSourceFullSum_run_signedFresh_cache_none, removing the unnecessary monad_norm rewriting step.
• VCVio/CryptoFoundations/ReplayFork.lean: Removed OracleSpec.toPFunctor from the local reducible attribute, so that definition no longer unfolds during simplification in this file; the comment was updated to explain the remaining PFunctor.Idx reducibility. In the proof of contextFork_success, two simp calls lost the unused lemma mem_support_freeM_pure_iff, slightly simplifying the proof script.
• VCVio/Interaction/UC/AsyncRuntime.lean: The diff renames all occurrences of the type Spec (and its sub‑types Spec.Sampler, Spec.Node.Context) to TypeTree throughout the file. This affects the ProcessScheduler abbreviation (its specOf parameter now expects TypeTree.{0} instead of Spec.{0}, and its sampler type becomes TypeTree.Sampler), the runStepsAsync function (its Γ context is now TypeTree.Node.Context and the procScheduler argument passes (process.step st.proc).tree instead of (process.step st.proc).spec), and the theorem runStepsAsync_empty_trivial_eq (its Γ and sampler types are updated accordingly). The documentation comments are also updated to reflect the new naming. No sorry or admit are introduced.
• VCVio/Interaction/UC/AsyncSecurity.lean: The AsyncRun structure was refactored to replace procTranscript (of type (process.step (state n).proc).spec.Transcript) with procPath (of type (process.step (state n).proc).tree.Path), and correspondingly updated field documentation and the next_state field's processTick branch to use procPath. The Γ type parameter throughout AsyncRun, its namespace, and all dependent declarations (enabledAt, firedAt, fired_implies_enabled, weakFair_on_strongFair_on, weakFair_of_strongFair) was changed from Spec.Node.Context to TypeTree.Node.Context. The enabledAt and firedAt definitions and their documentation were updated to reference tree.Path and procPath instead of spec.Transcript and procTranscript. The SchedulerPair structure's proc field signature changed from ProcessScheduler m p.Proc State (fun st => (p.step st.proc).spec) to ProcessScheduler m p.Proc State (fun st => (p.step st.proc).tree). No sorry or admit were added.
• VCVio/Interaction/UC/Runtime.lean: This commit renames the Spec type and its associated definitions to TypeTree across VCVio/Interaction/UC/Runtime.lean, reflecting a broader refactoring of the interaction framework's tree representation from Spec to TypeTree. Specifically, the namespace Spec is changed to TypeTree; Sampler.uniform now takes an explicit TypeTree.Nonempty spec argument alongside the existing TypeTree.Fintype spec, and Sampler.uniformI is updated to require both [TypeTree.Fintype spec] and [TypeTree.Nonempty spec] instances; the term Spec.sampleTranscript is replaced by TypeTree.samplePath; and StepOver.sample and ProcessOver.runSteps have their signatures updated to use TypeTree.Sampler, TypeTree.Node.Context, and step.tree in place of Spec.Sampler, Spec.Node.Context, and step.spec. Additionally, the module imports are updated to reflect the renamed file TypeTreeFintype, and the docstrings and comments throughout are revised to consistently refer to TypeTree instead of Spec, including the addition of a separate TypeTree.Nonempty smoke test example.
• VCVio/Interaction/UC/StdDoBridge.lean: The file renames the namespace Interaction.Spec to Interaction.TypeTree and updates all references accordingly: theorems sampleTranscript_done and sampleTranscript_node become samplePath_done and samplePath_node; all uses of Spec.Sampler become TypeTree.Sampler and Spec.Node.Context become TypeTree.Node.Context. In the example, the field name spec in the step record is changed to tree, and the corresponding sampler type is updated. Comments are adjusted to reflect that path sampling operates on TypeTree rather than Spec. These changes align the bridge with a prior refactor of the runtime primitives.
• VCVio/OracleComp/OracleComp.lean: The diff makes OracleComp @[reducible], adds the round-trip theorem ofFreeM_toFreeM and the ofFreeM_pure theorem (which states ofFreeM of FreeM.pure equals pure), and removes the now-redundant Monad, LawfulMonad, and MonadLift instances (the reducible definition means these are inherited from PFunctor.FreeM directly).
• VCVio/OracleComp/OracleQuery.lean: Made OracleQuery a @[reducible] definition, which makes its definitional unfolding transparent to the type checker, potentially improving type inference and unification. Removed the explicit Functor and LawfulFunctor instance declarations for OracleQuery spec that were forwarding to the underlying PFunctor.Obj instances; these instances are no longer needed because the reducible marker automatically provides them via the PFunctor.Obj instances through definitional transparency.
• VCVio/OracleComp/OracleSpec.lean: The toPFunctor definition was refactored from a structure literal to an explicit PFunctor.mk call and marked @[reducible] to improve definitional unfolding. The toPFunctor_add lemma had its @[simp] attribute removed, with an added doc comment explaining that rewriting with it inside the instance-carrying type of OracleComp can break simulateQ/liftM goal matching; the lemma itself is unchanged.
• VCVio/OracleComp/QueryTracking/HandlerSimp.lean: The file now imports PolyFun.PFunctor.Handler.Normalization and updates its module-level docstring to state that the handler_simp simp set supplements PolyFun's generic handler_nf normal form with VCVio-specific equations. To avoid duplication with that generic normalization, several StateT.run_* lemmas (run_bind, run_get, run_set, run_modifyGet, run_pure, run_monadLift) and a few WriterT.run_* lemmas (run_bind, run_pure, run_tell) are removed from the handler_simp attribute set; the remaining WriterT.run_bind', WriterT.run_monadLift, WriterT.run_monadLift', and WriterT.run_pure' are kept alongside the three oracle apply_eq lemmas. No sorry or admit are added.
• VCVio/OracleComp/SimSemantics/QueryImpl/Basic.lean: The QueryImpl definition’s docstring has been updated to describe it as a monadic handler for the polynomial interface induced by spec, replacing the previous explanation. The import PolyFun.PFunctor.Handler is added, and a new theorem eq_handler is introduced, stating that QueryImpl spec m is definitionally equal to PFunctor.Handler m spec.toPFunctor, thereby explicitly connecting the two representations.
• VCVio/OracleComp/SimSemantics/StateT/PreservesInv.lean: In simulateQ_run_preservesInv, the simpa block that derives hus' (showing us is in the support of (impl t).run σ0) was changed to use simulateQ_spec_query instead of the previous combination of OracleSpec.query_def and simulateQ_query. This likely reflects a consolidation of those two lemmas into a single simulateQ_spec_query lemma, simplifying the proof while maintaining the same logical step.
• VCVio/OracleComp/SimSemantics/StateT/StateSeparating.lean: Made Stateful a @[reducible] definition (line 41), added Stateful.eq_handler (lines 44-49) proving it equals PFunctor.Handler.Stateful (OracleComp I) σ E.toPFunctor, and added runState_eq_handler_run (lines 151-155) proving runState equals PFunctor.Handler.Stateful.run. These bridge the project's QueryImpl.Stateful to PolyFun's generic stateful-handler formalization, enabling reuse of PolyFun's theorems and constructions.
• VCVio/OracleComp/SimSemantics/WriterT/PreservesInv.lean: In the proof of simulateQ_run_writerPreservesInv, the query_bind case was updated by replacing the simp lemmas OracleSpec.query_def, ofPFunctor_toPFunctor, simulateQ_query, OracleQuery.input_apply, OracleQuery.cont_apply, and id_map with a single lemma simulateQ_spec_query. This simplifies the rewriting step and likely makes the proof more direct or more maintainable. No other changes were made; the theorem’s signature and the overall structure are unchanged.
• VCVio/OracleComp/Traversal.lean: Reimplemented the four traversal predicates (allPathsSatisfy, somePathSatisfies, allOutputsSatisfyWhen, someOutputSatisfiesWhen) and their associated lemmas (allPathsSatisfy_pure, somePathSatisfies_pure, allPathsSatisfy_query_bind, somePathSatisfies_query_bind, allPathsSatisfy_bind_iff, somePathSatisfies_bind_iff, allOutputsSatisfyWhen_iff_supportWhen, someOutputSatisfiesWhen_iff_supportWhen) to use a cursor-based formulation from PolyFun.PFunctor.Free.Cursor. The original inductive definitions over OracleComp.construct are replaced by quantification over PFunctor.FreeM.Cursor with TraceList.DirectionsWithin and FreeM.RootSatisfies (imported from the new PolyFun dependency). The lemma proofs are rewritten to use cursor manipulation, and the allOutputsSatisfyWhen/someOutputSatisfiesWhen definitions now call the top-level allPathsSatisfy/somePathSatisfies instead of using dot notation.
• VCVio/Prelude.lean: Updated the doc comment for the handler_simp simp attribute from a generic description to explicitly state it is a VCVio-specific extension of PolyFun's handler_nf normalization set.
• VCVio/ProgramLogic/Tactics/Common/Core.lean: The diff adds an import of Lean.Meta.Sym.Pattern and defines a new function symMatchKey that normalizes reducible oracle wrappers (OracleComp, OracleQuery, OracleSpec.toPFunctor) in a goal-side expression, unfolding them so that structural key matching in Sym.DiscrTree.getMatch works correctly. The docstring explains that Sym.preprocessType is intentionally avoided because it can cause panics in Lean 4.32 when unfolding user programs containing matchers with loose de Bruijn indices.
• VCVio/ProgramLogic/Tactics/Common/Registry.lean: In VCVio/ProgramLogic/Tactics/Common/Registry.lean, three lookup functions now apply symMatchKey to normalize the expression before querying the Sym discrimination tree. getRegisteredUnaryVCSpecEntries adds let comp ← symMatchKey comp after whnfReducible; getRegisteredUnaryVCSpecEntriesNoWhnf replaces instantiateMVars comp with symMatchKey comp; and getRegisteredRelationalVCSpecEntries wraps the existing whnfReducible expression with symMatchKey for oa. This change ensures consistent key normalization across all VC spec entry lookups, affecting which entries match during tactic dispatch.
• VCVio/ProgramLogic/Tactics/Common/WpStepRegistry.lean: The getRegisteredWpStepEntries function now applies symMatchKey to the expression after whnf (and after instantiateMVars), while getRegisteredWpStepEntriesNoWhnf replaces its prior instantiateMVars call with a symMatchKey call, removing instantiateMVars entirely. These changes adjust the preprocessing of expressions before they are matched against the wpStepRegistry, shifting from metadata instantiation to symbol-key transformation, which affects how wp tactic dispatch resolves rewrite entries for both normalized and raw expression paths.
• VCVio/ProgramLogic/Tactics/Handler.lean: The handler_step tactic’s implementation now invokes simp only [handler_nf, handler_simp] instead of the previous handler_simp alone, and its docstring has been updated to reflect that the normalization pass uses PolyFun’s generic handler_nf set followed by VCVio’s handler_simp extension. This change broadens the set of rewrite rules applied during a single normalization step.
• VCVio/StateSeparating/CellRef.lean: In the proof of simulateQ_run_cellPreserved, the simpa call was simplified by removing OracleSpec.query_def from the list of rewriting lemmas, leaving only simulateQ_spec_query. This avoids an unnecessary unfold of OracleSpec.query, streamlining the proof without changing its logical content.
• docs/agents/gotchas.md: Summary unavailable — AI generation failed.
• docs/agents/oracle-comp.md: The documentation now explains that QueryImpl is definitionally equivalent to PFunctor.Handler m spec.toPFunctor, recorded by QueryImpl.eq_handler. It also introduces the PolyFun theorem, which asserts that the same object can interpret any free program over the interface, and clarifies that the dependent‑function form is retained to improve expected‑type inference for polymorphic query code.
• docs/agents/program-logic.md: The documentation for handler_step now lists FreeM among the supported goal types and includes handler_nf in its normalization pass. A new paragraph clarifies that PolyFun owns generic handler_nf rules for FreeM, StateT, and WriterT, while VCVio's handler_simp adds oracle‑simulation and caching equations; handler_step composes both sets. A new subsection titled Key alignment invariant explains that Sym.DiscrTree.getMatch requires structural term matching, so registry query functions route extracted computations through symMatchKey (which unfolds only OracleComp, OracleQuery, and OracleSpec.toPFunctor) to avoid silent lookup failures that manifest as vcstep reporting “no matching rule applied” despite a working manual rewrite.
• 2 file(s) filtered as noise (lockfiles, generated, or trivial): lake-manifest.json, lakefile.lean